Nuprl Definition : interface
11,40
postcript
pdf
interface(
ds
;
da
;
A
) == fpf(LocKnd;
ik
.locknd-spread(
ik
;
i
,
k
.(
ds
(
i
)
da
(
i
,
k
)
(
A
+ top))))
latex
Definitions
fpf(
A
;
a
.
B
(
a
))
,
LocKnd
,
locknd-spread(
ik
;
i
,
k
.
P
(
i
;
k
))
,
x
:
A
B
(
x
)
,
f
(
a
)
,
left
+
right
,
top
FDL editor aliases
interface
origin
da(i,k)(A + top)))) da(i,k)(A + top)))) B(x)